(declare-fun c () (_ BitVec 32))
(declare-fun d (Int Int) Int)
(declare-fun a () (_ BitVec 32))
(declare-fun oh () Bool)
(declare-fun ih () Bool)
(declare-fun of () Bool)
(declare-fun if () Bool)
(declare-fun aa () (_ BitVec 32))
(declare-fun k () (_ BitVec 32))
(declare-fun ka () (_ BitVec 32))
(declare-fun b () (_ BitVec 32))
(declare-fun ba () (_ BitVec 32))
(declare-fun l () (_ BitVec 32))
(declare-fun la () (_ BitVec 32))
(declare-fun mh () (_ BitVec 32))
(declare-fun jh () (_ BitVec 32))
(declare-fun ac () Bool)
(declare-fun jf () (_ BitVec 32))
(declare-fun ad () Bool)
(assert (not (= (not ih) (bvslt l c) (bvslt la c) (= (= b ba) (or (distinct a aa) (distinct k ka) (distinct l la))) (= (d 0 7) 7) (=> (not oh) (= jh #x00000000)) (or ac (=> (= (d 0 7) 0) (= (not ih) (= mh #x00000000)) (= mh #x00000000)) (=> (=> of (= jf #x00000005) ad (= (= (d 0 4117) 0) (not if))) (=> (not if) (= (d 0 4117) 0) (not of) (= jf #x00000000)))))))
(check-sat)
